1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
#![forbid(missing_debug_implementations, missing_docs, unsafe_code)]
pub mod ast;
pub mod builder;
pub mod ctx;
pub mod error;
pub mod primitive;
pub mod program;
pub mod repr;
pub mod term;
pub mod typing;
pub mod utils;
pub use error::Error;
pub mod prelude {
use crate::*;
pub use ctx::{
cons::ConsCtx,
eq::{DisjointSetCtx, Structural, TermEqCtx, TermEqCtxEdit, TermEqCtxMut, Typed, Untyped},
eval::{NormalCfg, Reduce, ReduceUntil, ReductionConfig},
subst::{EvalCtx, Shift, SubstCtx, SubstSlice, SubstVec},
ty::{BinaryCtx, Trivial, TrivialCons, TyCtxMut, TRIVIAL},
StandardCtx,
};
pub use program::NodeIx;
pub use term::{
dynamic::{DynamicTerm, DynamicValue},
flags::{AtomicTyckFlags, TyckFlag, TyckFlags},
weak::WeakId,
Annotation, AnnotationLike, AnnotationRef, App, Case, Cons, Enum, Form, HasDependencies,
Id, Lambda, OptionalValue, Pi, Refl, Substitute, Term, TermEq, TermId, Typecheck, Universe,
UniverseTerm, Value, Var, VarFilter, Variant,
};
}
use prelude::*;
use ahash::AHasher;
use ctx::ty::MapTyCtx;
use enum_iterator::IntoEnumIterator;
use lazy_static::lazy_static;
use log::*;
use primitive::logical::*;
use smallvec::{smallvec, SmallVec};
use smol_str::SmolStr;
use std::any::Any;
use std::borrow::Borrow;
use std::borrow::Cow;
use std::cmp::Ordering;
use std::cmp::Ordering::*;
use std::convert::TryFrom;
use std::fmt::{self, Debug, Display, Formatter};
use std::hash::{BuildHasherDefault, Hash, Hasher};
use std::ops::*;
use std::sync::atomic::Ordering::*;
use std::sync::{Arc, Weak};
use term::flags::*;
use term::Code;
use utils::*;
use TyckFlag::*;